import {operatorAdd} from './functional.js'
import {pipe, zip, every, reduce, makeContinuable, take} from './iterator.js'
import {type MetaMap, type BoundMap, type VariableTerm, type QuantifiedVariableTerm, Term} from './term.js'
import type {PredicateSpecification} from './predicateSpecification.js'
import {serializeList} from './serializeList.js'
import type {Type} from './type.js'

const enum Precedence {
    most,
    not,
    '&',
    or,
    implies,
    iff,
    quantor,
    least,
}

export abstract class Formula {
    abstract unify(other: Formula, metaMap: MetaMap, boundMap: BoundMap): boolean
    abstract serialize(outerPrecedence?: Precedence, isLeftSide?: boolean): Iterable<string>
    abstract substitute(map: Map<Term, Term>): Formula
}

function isSameConstructor<T extends object>(x: T, y: object): y is T {
    return x.constructor == y.constructor
}

export namespace Formula {
    export abstract class Constant extends Formula {
        unify(other: Formula, metaMap: MetaMap, boundMap: BoundMap) {
            return this.constructor === other.constructor
        }

        substitute() {
            return this
        }
    }

    export const True = new class extends Constant {
        * serialize() {
            yield 'true'
        }
    }

    export const False = new class extends Constant {
        * serialize() {
            yield 'false'
        }
    }

    export abstract class Binary extends Formula {
        private static readonly operationMap = {
            '&': Precedence['&'],
            or: Precedence.or,
            implies: Precedence.implies,
            iff: Precedence.iff,
        }

        readonly operands: [Formula, Formula]

        constructor(operands: [Formula, Formula]) {
            super()
            this.operands = operands
        }

        unify(other: Formula, metaMap: MetaMap, boundMap: BoundMap): boolean {
            if (!isSameConstructor(this, other))
                return false

            return pipe(
                zip(this.operands, other.operands),
                every(([operand1, operand2]) => operand1.unify(operand2, metaMap, boundMap)),
            )
        }

        substituteOperands(map: Map<Term, Term>): [Formula, Formula] {
            return [
                this.operands[0].substitute(map),
                this.operands[1].substitute(map),
            ]
        }

        protected static* serializeHelper(
            connective: '&' | 'or' | 'implies' | 'iff',
            operands: [Formula, Formula],
            outerPrecedence: Precedence,
            isLeftSide: boolean,
        ): Iterable<string> {
            const precedence = Binary.operationMap[connective]

            if (precedence > outerPrecedence || precedence == outerPrecedence && isLeftSide)
                yield '('

            yield* operands[0].serialize(precedence, true)
            yield ' '
            yield connective
            yield ' '
            yield* operands[1].serialize(precedence)

            if (precedence > outerPrecedence || precedence == outerPrecedence && isLeftSide)
                yield ')'
        }
    }

    export class Conjunction extends Binary {
        substitute(map: Map<Term, Term>) {
            return new Conjunction(this.substituteOperands(map))
        }

        * serialize(outerPrecedence = Precedence.least, isLeftSide = false) {
            const [left, right] = this.operands
            const boundMap: BoundMap = new Map
            const metaMap: MetaMap = new Map
            const isEquivalence = left instanceof Implication && right instanceof Implication &&
                left.operands[0].unify(right.operands[1], metaMap, boundMap) &&
                left.operands[1].unify(right.operands[0], metaMap, boundMap)

            yield* isEquivalence
                ? Binary.serializeHelper('iff', left.operands, outerPrecedence, isLeftSide)
                : Binary.serializeHelper('&', this.operands, outerPrecedence, isLeftSide)
        }
    }

    export class Disjunction extends Binary {
        substitute(map: Map<Term, Term>) {
            return new Disjunction(this.substituteOperands(map))
        }

        * serialize(outerPrecedence = Precedence.least, isLeftSide = false) {
            yield* Binary.serializeHelper('or', this.operands, outerPrecedence, isLeftSide)
        }
    }

    export class Implication extends Binary {
        substitute(map: Map<Term, Term>) {
            return new Implication(this.substituteOperands(map))
        }

        * serialize(outerPrecedence = Precedence.least, isLeftSide = false) {
            if (this.operands[1] == False) {
                yield 'not '
                yield* this.operands[0].serialize(Precedence.not)
            } else
                yield* Binary.serializeHelper('implies', this.operands, outerPrecedence, isLeftSide)
        }
    }

    export class Predicate extends Formula {
        readonly specification: PredicateSpecification
        readonly parameters: Term[]

        constructor(specification: PredicateSpecification, parameters: Term[]) {
            super()
            this.specification = specification
            this.parameters = parameters
        }

        unify(other: Formula, metaMap: MetaMap, boundMap: BoundMap): boolean {
            return other instanceof Predicate &&
                this.specification === other.specification &&
                Term.unifyLists(this.parameters, other.parameters, metaMap, boundMap)
        }

        substitute(map: Map<Term, Term>) {
            return new Predicate(
                this.specification,
                this.parameters.map(parameter => parameter.substitute(map)),
            )
        }

        * serialize() {
            const parameterIterator = pipe(this.parameters, makeContinuable)
            const {symbolOffset, name} = this.specification

            yield* serializeList(
                take(symbolOffset)(parameterIterator),
                term => term.serialize(),
            )

            if (symbolOffset > 0)
                yield ' '

            yield name

            if (this.specification.parameterTypes.length > symbolOffset)
                yield ' '

            yield* serializeList(parameterIterator, term => term.serialize())
        }
    }

    export class Equality extends Formula {
        readonly left: Term
        readonly right: Term

        constructor(left: Term, right: Term) {
            super()
            this.left = left
            this.right = right
        }

        unify(other: Formula, metaMap: MetaMap, boundMap: BoundMap): boolean {
            return other instanceof Equality &&
                this.left.unify(other.left, metaMap, boundMap) &&
                this.right.unify(other.right, metaMap, boundMap)
        }

        substitute(map: Map<Term, Term>) {
            return new Equality(
                this.left.substitute(map),
                this.right.substitute(map),
            )
        }

        * serialize() {
            yield* this.left.serialize()
            yield ' = '
            yield* this.right.serialize()
        }
    }

    export class TypeAssertion extends Formula {
        readonly type: Type
        readonly parameter: Term

        constructor(parameter: Term, type: Type) {
            super()
            this.type = type
            this.parameter = parameter
        }

        unify(other: Formula, metaMap: MetaMap, boundMap: BoundMap): boolean {
            return other instanceof TypeAssertion &&
                this.type === other.type &&
                this.parameter.unify(other.parameter, metaMap, boundMap)
        }

        substitute(map: Map<Term, Term>) {
            return new TypeAssertion(
                this.parameter.substitute(map),
                this.type,
            )
        }

        * serialize() {
            yield* this.parameter.serialize()
            yield ' is '
            yield this.type.name
        }
    }

    export abstract class Quantor extends Formula {
        variable: QuantifiedVariableTerm
        operand: Formula

        constructor(variable: QuantifiedVariableTerm, operand: Formula) {
            super()
            this.variable = variable
            this.operand = operand
        }

        unify(other: Formula, metaMap: MetaMap, boundMap: BoundMap): boolean {
            if (!isSameConstructor(this, other) || this.variable.type != other.variable.type)
                return false

            boundMap.set(this.variable, other.variable)

            return this.operand.unify(other.operand, metaMap, boundMap)
        }
    }

    export class Generalization extends Quantor {
        substitute(map: Map<Term, Term>) {
            return new Generalization(
                this.variable.substitute(map) as QuantifiedVariableTerm,
                this.operand.substitute(map),
            )
        }

        * serialize(outerPrecedence: Precedence, isLeftSide: boolean): Iterable<string> {
            yield 'for '

            let formula: Formula = this

            yield* serializeList(
                (function* () {
                    for (; formula instanceof Generalization; formula = formula.operand)
                        yield formula.variable
                }()),
                serializeQuantifiedVariable,
            )

            if (formula instanceof Implication) {
                yield ' st '
                yield* formula.operands[0].serialize(Precedence.quantor, true);

                [, formula] = formula.operands
            }

            yield formula instanceof Existence
                ? ' '
                : ' holds '

            yield* formula.serialize(Precedence.quantor)
        }
    }
    export class Existence extends Quantor {
        substitute(map: Map<Term, Term>) {
            return new Existence(
                // @ts-expect-error fix this weak typing
                this.variable.substitute(map),
                this.operand.substitute(map),
            )
        }

        * serialize(outerPrecedence: Precedence, isLeftSide?: boolean | undefined) {
            yield 'ex '

            let formula: Formula = this

            yield* serializeList(
                (function* () {
                    for (; formula instanceof Existence; formula = formula.operand)
                        yield formula.variable
                }()),
                serializeQuantifiedVariable,
            )

            yield ' st '
            yield* formula.serialize(Precedence.quantor)
        }
    }
}

export function* serializeQuantifiedVariable(variable: VariableTerm) {
    yield variable.name
    yield ' be '
    yield variable.type.name
}

export const stringify = (formula: Formula) => pipe(formula.serialize(), reduce(operatorAdd))
